Формализация языков частично упорядоченных мультимножеств в системе Coq для спецификации слабых моделей памяти
Аннотация:
Предмет исследования. Модели памяти задают семантику многопоточных программ, работающих с разделяемой памятью. В настоящее время эта область активно развивается, создаются новые модели памяти, востребованы новые средства формализации таких моделей, а также способы и средства доказательства их свойств. В работе рассмотрена задача формальной спецификации моделей памяти в системах интерактивного доказательства теорем. Метод. Использован семантический домен языков частично упорядоченных мультимножеств или языков помсетов. Предложен метод кодировки семантического домена с помощью фактор-типов и обсуждены его достоинства и недостатки. Основные результаты. Представлена библиотека, разработанная в системе Coq, реализующая предложенный метод. В рамках библиотеки установлена взаимосвязь языков помсетов с традиционной операционной семантикой, заданной в терминах помеченных систем переходов. Это позволило специфицировать в Coq модели памяти, параметризованные операционной семантикой структуры данных, и, таким образом, разделить определения модели памяти и структуры данных. Практическая значимость. Предложенная библиотека может быть использована для формальной спецификации и доказательства свойств широкого класса моделей памяти. Чтобы продемонстрировать это, в работе приведена формализация нескольких базовых моделей, а именно, моделей последовательной, причинной и конвейерной согласованности.
Ключевые слова:
Постоянный URL
Статьи в номере
- Методы аудиовизуального распознавания людей в масках
- Влияние соотношения интенсивностей опорной и объектной волн на распределение интенсивности в формируемом с их помощью голографическом поле
- Высокоточный волоконно-оптический датчик температуры на основе интерферометра Фабри–Перо с отражающими тонкопленочными многослойными структурами
- Метод проектирования оптической системы для концентрации излучения мощных светодиодов
- Обнаружения выбоин на дорожных покрытиях с использованием методов фотограмметрии и дистанционного зондирования
- Адаптивное управление нелинейным объектом с несогласованными параметрическими неопределенностями и ограничением на входное воздействие
- Применение методов детектирования отказов для обнаружения информационных атак на систему управления
- Алгоритм детектирования и локализации отказов двигателя постоянного тока
- Синтез и реализация λ -подхода скользящего управления в системе теплопотребления
- Фотокаталитические свойства наноструктур Ag–AgBr в ионообменном слое натриево-цинк-алюмосиликатного стекла с бромом
- Облачная интеллектуальная система мониторинга для обнаружения нарушений маски и выдачи предупреждений
- Эффективная инкрементная хеш-цепочка с вероятностным методом на основе фильтра для обновления легких узлов блокчейна
- Метод генерации масок на изображениях лиц и системы их распознавания
- Повышение эффективности обработки жестового языка посредством малокадрового машинного обучения
- Комплекснозначное разложение матричных данных на принципах квантовой теории
- Моделирование базового переводчика индонезийского языка жестов на одноплатном компьютере Raspberry Pi
- Метод многомодального машинного сурдоперевода для естественного человеко-машинного взаимодействия
- Веб-приложение для быстрой оценки субъективных ответов с использованием обработки естественного языка
- Обоснование путей построения и оценка эффективности применения пространственно распределенной системы информационных сенсоров для мониторинга обстановки
- Мониторинг инфильтрационных процессов в гидротехнических сооружениях с использованием распределенного акустического сенсора
- Конструкция волноводной антенны с прорезями для морской радиолокационной системы